T:Type, f:(TT), L:(T List), x, y, z:T. z=f*(x) via L  (y  L)  (f(y) = y)  (y = z) 

latex

Definitions

type List, t  T, s = t, Type, x:AB(x), y=f*(x) via L, (x  l), P  Q, x:A. B(x), ||as||, n+m, a < b, {i..j}, #$n, [], Void, False, A, A  B, , , b, l[i], , f(a), {x:A| B(x)} , x:A  B(x), P & Q, -n, last(L), A c B, <a, b>, , P  Q, hd(l), x:A. B(x), [car / cdr], left + right, P  Q, A List, n - m, tl(l), if a<b then c else d, i <z j, b, i z j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , nth_tl(n;as), rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, P  Q, {T}, i  j

Lemmas

fun-path-cons, non neg length, length wf1, cons member, nil member, last wf, int seg wf, not wf, select wf, member wf, assert wf, length wf2, l member wf, fun-path wf